package edu.lambdateacher.expressions;

/*
 LambdaTeacher
 Copyright (C) 2000  Kim Mason
 Copyright (C) 2014  Vitalij Zadneprovskij

 This program is free software; you can redistribute it and/or
 modify it under the terms of the GNU General Public License
 as published by the Free Software Foundation; either version 2
 of the License, or (at your option) any later version.

 This program is distributed in the hope that it will be useful,
 but WITHOUT ANY WARRANTY; without even the implied warranty of
 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 GNU General Public License for more details.

 You should have received a copy of the GNU General Public License
 along with this program; if not, write to the Free Software
 Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
 */

import java.util.HashSet;
import java.util.Set;

import edu.lambdateacher.PropertiesManager;
import edu.lambdateacher.reductions.EtaReduction;

/**
 * The class Abstraction represents a Lambda Abstraction. It is a subclass of
 * Expression. An Abstraction is of the form \bound_var.body, where bound_var is
 * a string, and body is an Expression. Abstractions are eta reducable.
 */
public class Abstraction extends Expression implements Cloneable {
	private String boundVar;
	private Expression body;

	/**
	 * A simple constructor function. Sets the bound variable and the body to
	 * null.
	 */
	public Abstraction() {
		super(); // this is implicit anyway
		setBoundVar(null);
		setBody(null);
	}

	/**
	 * This constructor sets both the bound variable and the body.
	 */
	public Abstraction(String invar, Expression inbody) {
		super();
		this.setBoundVar(invar);
		this.setBody(inbody);
	}

	/**
	 * Sets the bound variable of the abstraction, but not the body.
	 */
	public Abstraction(String invar) {
		this();
		setBoundVar(invar);
	}

	/**
	 * getBoundVar simply returns the bound variable of this Abstraction. It
	 * returns the actual String, not a copy.
	 */
	public final String getBoundVar() {
		return this.boundVar;
	}

	public final void setBoundVar(String instring) {
		this.boundVar = instring;
	}

	public final Expression getBody() {
		return this.body;
	}

	/** 
	 * getBodySkipBindings skips over any bindings to
	 * get the body */
	public final Expression getBodySkipBindings() {
		Expression tempexpr;

		tempexpr = this.getBody();
		while (tempexpr instanceof Binding) {
			tempexpr = ((Binding) tempexpr).getExpr();
		}
		return tempexpr;
	}

	public final void setBody(Expression inbody) {
		body = inbody;
		if (body != null) {
			if (body.getParentModified()) {
				this.setParentModified(true);
			}
		}
	}

	/**
	 * containsUnbound returns true if a variable with name matching inname
	 * exists unbound within this abstraction, otherwise returns false.
	 */
	@Override
	public boolean containsUnbound(String inname) {
		if (inname == null) {
			return false;
		}

		Expression thebody = this.getBody();
		if (thebody == null) {
			return false;
		}

		// if the inname is the same as the bound variable,
		// return false (it's now bound).
		if (inname.equals(this.getBoundVar())) {
			return false;
		}

		// it's not bound so far, so check if it exists unbound in
		// the body of this abstraction.
		return thebody.containsUnbound(inname);
	}

	/**
	 * eta_allowed returns true if eta reduction can be performed on this
	 * expression. Note that the reduction must be direct, not on the leftmost
	 * redex. This means that the body of this expression must be an
	 * application. The arg of that application must be a variable with the same
	 * name as the bound variable of this Abstraction. The func of that
	 * application can't contain the bound variable of this abstraction as an
	 * unbound variable.
	 */
	@Override
	public boolean etaAllowed() {
		String curboundvar = this.getBoundVar();
		if (curboundvar == null) {
			return false;
		}

		Expression thebody = this.getBodySkipBindings();

		return EtaReduction.etaAllowed(curboundvar, thebody);
	}

	/**
	 * eta_reduce() checks if eta reduction is allowed. If it is, the body of
	 * this Abstraction is found, it's func is returned (not a clone).
	 * parentmodified is set to true in the return expression, as eta reducing
	 * should destroy any bindings above it.
	 */
	@Override
	public Expression etaReduce() {
		return EtaReduction.etaReduce(this);
	}

	/**
	 * Override the clone method in superclass Object. clone() recursively
	 * copies the Abstraction (it clones its bound variable and body, then
	 * returns a new abstraction composed of these clones).
	 */
	@Override
	public Object clone() {
		Abstraction toreturn = (Abstraction) super.clone();
		Expression thebody = null;
		String thevar = null;

		// clone the body of this abstraction
		if (this.getBody() != null) {
			thebody = (Expression) getBody().clone();
		}

		// set the bound variable of the new abstraction
		if (this.getBoundVar() != null) {
			thevar = new String(this.getBoundVar());
		}
		toreturn.setBoundVar(thevar);
		toreturn.setBody(thebody);
		return toreturn;
	}

	/**
	 * unParse() simply returns a string with the current Abstraction unparsed
	 * into it. if verbose then use all brackets
	 */
	@Override
	public String stringRepresentation(boolean verbose) {
		String thestring = "(" + PropertiesManager.LAMBDA_CHAR;
		String b_var = getBoundVar();
		if (b_var != null) {
			thestring = thestring + b_var;
		}
		thestring = thestring + ".";

		Expression thebody = this.getBody();
		if (thebody != null) {
			thestring = thestring + thebody.stringRepresentation(verbose);
		}
		thestring = thestring + ")";
		return thestring;
	}

	/**
	 * name_substitute searches for an unbound Variable with the same name as
	 * inname within the current Abstraction, and replaces it with a clone of
	 * param. It returns the new expression as the result. Note that only the
	 * input param is ever cloned (this is string reduction, not graph
	 * reduction). Read Section 12 of The Implementation of Functional
	 * Programming Languages by Peyton Jones for more info.
	 */
	@Override
	public Expression nameSubstitute(String inname, Expression param) {
		// we can't sub for a name which doesn't exist.
		if (inname == null) {
			return this;
		}

		// check if the variable is now bound, so we can't name substitute.
		if (inname.equals(this.getBoundVar())) {
			return this;
		}

		// the body is null, so no name substitution can occur
		Expression oldbody = this.getBody();
		if (oldbody == null) {
			return this;
		}

		// the name doesn't exist unbound in the body, and
		// so can't be substituted for.
		if (oldbody.containsUnbound(inname) == false) {
			return this;
		}

		// if there are no free occurences of the bound variable
		// in the parameter to sub in, then just sub the param
		// into the body, and return this abstraction with the
		// new body
		Expression toreturn = null;
		Expression newbody = null;
		if (param.containsUnbound(this.getBoundVar()) == false) {
			newbody = oldbody.nameSubstitute(inname, param);
			toreturn = this;
			((Abstraction) toreturn).setBody(newbody);
			return toreturn;
		}

		// if we've made it to here, the bound variable of the current
		// abstraction occurs free in tosub, and so we have to RENAME
		// the bound variable before substitution. As you can see,
		// this is a recursive problem. We must rename it with a name
		// which doesn't occur free in the body or the param.
		String newname = "";

		// while the body or the param contain the name unbound, then ask for it
		// again (and again, and again, if necessary).
		while (oldbody.containsUnbound(newname) || param.containsUnbound(newname)) {
			String messagestring = "";
			if (param.containsUnbound(newname)) {
				messagestring = messagestring + "The new name clashes with the expression being substituted in:\n";
				messagestring = messagestring + param.stringRepresentation(false) + "\n";
			}

			if (oldbody.containsUnbound(newname)) {
				messagestring = messagestring + "The new name clashes with the expression being modified:\n";
				messagestring = messagestring + oldbody.stringRepresentation(false) + "\n";
			}

			messagestring = messagestring + "Please enter a new name.";

		}

		// now we've got a valid name to rename the bound variable with, so
		// rename the bound variable
		String oldboundvar = this.getBoundVar();
		this.setBoundVar(newname);
		Variable tosubin = new Variable(newname);
		// now rename the variable!
		newbody = oldbody.nameSubstitute(oldboundvar, tosubin);

		// now sub the param in for inname
		Expression newbodyone = newbody.nameSubstitute(inname, param);

		this.setBody(newbodyone);
		return this;
	}

	/**
	 * containsReducable returns true if the current Abstraction is a reducable
	 * expression (eta), or contains a reducable expression.
	 */
	@Override
	public boolean containsReducable() {
		// if this Abstraction is eta reducable, return true.
		if (this.etaAllowed()) {
			return true;
		}

		return this.getBody().containsReducable();
	}

	/**
	 * Normal reduce tries to eta reduce the current Abstraction. If it can't,
	 * it tries to normal_reduce the leftmost outermost expression (in this
	 * case, the body).
	 */
	@Override
	public Expression normalReduce() {
		// reduce the current abstraction if possible
		if (etaAllowed() == true) {
			return this.etaReduce();
		}

		Expression oldbody = this.getBody();

		if (oldbody == null) {
			return this;
		}

		// normal reduce the body
		Expression newbody = oldbody.normalReduce();

		Abstraction toreturn = this;
		toreturn.setBody(newbody);

		return toreturn;
	}

	/*
	 * reduceExpression simply searches for inexpr, and if the current
	 * expression is equal to inexpr, it reduces it and returns the result.
	 */
	@Override
	public Expression reduceExpression(Expression inexpr) {
		// if this is the expression to reduce
		if (inexpr == this) {
			Expression toreturn = this.etaReduce();
			return toreturn;
		}

		// call reduceExpression on the body of this abstraction, and replace
		// the
		// old body with the new body
		Expression oldbody = this.getBody();

		if (oldbody == null) {
			return this;
		}

		// attempt to reduce the body
		Expression newbody = oldbody.reduceExpression(inexpr);

		Abstraction toreturn = this;
		toreturn.setBody(newbody);

		return toreturn;
	}

	/**
	 * If this Abstraction is reducable, it is returned. Otherwise, the body's
	 * findNormalReducable is called.
	 */
	@Override
	public Expression findNormalReducable() {
		if (this.etaAllowed()) {
			return this;
		}

		if (this.getBody() == null) {
			return null;
		}

		return this.getBody().findNormalReducable();
	}

	/**
	 * findApplicativeReducable attempts to find the applicative reducable
	 * subexpression of the current Expression
	 */
	@Override
	public Expression findApplicativeReducable() {
		if (this.etaAllowed())
			return this;

		if (this.getBody() == null)
			return null;

		return this.getBody().findApplicativeReducable();
	}

	/**
	 * findUnboundVars returns a HashSet with the names of all of the unbound
	 * variables in the current expression. The input HashSet (bound_vars)
	 * contains all of the variable names that are bound.
	 */
	@Override
	public Set findUnboundVars(Set bound_vars) {
		// clone the input vector so that it isn't modified.
		HashSet theboundvars = new HashSet(bound_vars);

		// add the current bound var to the list
		// of elements
		if (this.getBoundVar() != null)
			theboundvars.add(new String(this.getBoundVar()));

		if (this.getBody() == null){
			return new HashSet();
		}

		return this.getBody().findUnboundVars(theboundvars);
	}

	/*
	 * removeAllBindings walks down the expression tree, and removes any
	 * bindings that it finds.
	 */
	@Override
	public Expression removeAllBindings() {
		Expression oldbody = this.getBody();

		if (oldbody == null)
			return this;

		Expression newbody = oldbody.removeAllBindings();
		this.setBody(newbody);
		return this;
	}

	/*
	 * removeBinding walks down the expression tree, and removes any occurences
	 * of the input parameter binding(toremove), replacing it with the
	 * expression toremove points to.
	 */
	@Override
	public Expression removeBinding(Binding toremove) {
		Expression oldbody = this.getBody();

		if (oldbody == null)
			return this;

		Expression newbody = oldbody.removeBinding(toremove);
		this.setBody(newbody);
		return this;
	}
	
	public Expression betaReduce(Application application){
		boolean involveabs = true;
		// first, get the expression to sub in
		Expression tosubin = application.getArg();

		// get the variable to replace
		String tosubfor = this.getBoundVar();

		// make copies of function and arg strings
		if (PropertiesManager.expdlogon) {
			String thisstr = application.stringRepresentation(false);
			String funcstr = this.stringRepresentation(false);
			String argstr = tosubin.stringRepresentation(false);
			String bvar = new String(tosubfor);
		}

		// name substitute the argument into the function body
		Expression thefuncbody = this.getBody();

		Expression toreturn;
		// something weird has happened if this is true.
		if (thefuncbody == null){
			toreturn = application;
		}else{
			toreturn = thefuncbody.nameSubstitute(tosubfor, tosubin);
		}
		
		return toreturn;
	}

}
